SYNTHESIZER: Add counterexample-guided loop assigns synthesis #7448
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
qinheping
requested review from
tautschnig,
feliperodri and
remi-delmas-3000
as code owners
qinheping
added
aws
Codecov ReportBase: 78.46% // Head: 78.47% // Increases project coverage by
Additional details and impacted files@@ Coverage Diff @@
## develop #7448 +/- ##
===========================================
+ Coverage 78.46% 78.47% +0.01%
===========================================
Files 1662 1662
Lines 190904 191013 +109
===========================================
+ Hits 149794 149899 +105
- Misses 41110 41114 +4
Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here. ☔ View full report at Codecov. |
jimgrundy
reviewed
Dec 20, 2022
qinheping
force-pushed
the
goto-synthesizer
branch
from
964964f to
184821a
Compare
tautschnig
approved these changes
Dec 20, 2022
src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp
Outdated
Show resolved
Hide resolved
qinheping
force-pushed
the
goto-synthesizer
branch
from
184821a to
4dee40e
Compare
Implement the functionality described below. Motivation --- This loop assigns synthesizer use the idea counter-example-guided synthesis (CEGIS) to synthesize loop assigns targets. It is based on the same CEGIS framework as the loop invariant synthesizer w ith the following difference. Use Cases --- Our loop invariants synthesizer will synthesize invariants clauses for all loops without loop invariant annotation. The loop assigns synthesizer will synthesize assigns clauses for all loops without loop invariant annotation **and** loop assigns annotation. Cause Loop ID --- In the loop invariant synthesizer, we say a loop is a cause loop if the violation is dependent on the loop's havoc instructions. Because invariant clauses affect the havoced values which could flow into variables outside the loop. In the loop assigns synthesizer, we say a loop is a cause loop if the violation is in the loop. Because assigns clauses only affect the CAR of its own loop body. Synthesizer --- For an assignable violation with checked target `T`, the new assigns target will be `T`. If `T` is a non-constant target, e.g., `ptr[i]` with `i` also an assigns target, we widen it to `__CPROVER_POINTER_OBJECT(T)`. We add the new target to cause loop one by one starting from the most-inner one. Until the assignable violation is resolved.
qinheping
force-pushed
the
goto-synthesizer
branch
from
4dee40e to
251c257
Compare
4 tasks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Implement the functionality described below.
Motivation
This loop assigns synthesizer use the idea counter-example-guided synthesis (CEGIS) to synthesize loop assigns targets. It is based on the same CEGIS framework as the loop invariant synthesizer w ith the following difference.
Use Cases
Our loop invariants synthesizer will synthesize invariants clauses for all loops without loop invariant annotation. The loop assigns synthesizer will synthesize assigns clauses for all loops without loop invariant annotation and loop assigns annotation.
Cause Loop ID
In the loop invariant synthesizer, we say a loop is a cause loop if the violation is dependent on the loop's havoc instructions. Because invariant clauses affect the havoced values which could flow into variables outside the loop. In the loop assigns synthesizer, we say a loop is a cause loop if the violation is in the loop. Because assigns clauses only affect the CAR of its own loop body.
Synthesizer
For an assignable violation with checked target
T, the new assigns target will beT. IfTis a non-constant target, e.g.,ptr[i]withialso an assigns target, we widen it to__CPROVER_POINTER_OBJECT(T). We add the new target to cause loop one by one starting from the most-inner one. Until the assignable violation is resolved.